WARNING:  Note that the rewrite rule INVERSE-IS-UNIQUE will be stored
so as to apply only to terms with the nonrecursive function symbol
INVERSE.


WARNING:  Note that INVERSE-IS-UNIQUE contains the free variable X
which will be chosen by instantiating the hypothesis:
      (EQUAL 1. (REMAINDER (TIMES M X) P))
.


WARNING:  Note that the rewrite rule SUB1-P-IS-INVOLUTION will be
stored so as to apply only to terms with the nonrecursive function
symbol INVERSE.


WARNING:  Note that the rewrite rule N-O-I-LEMMA2 will be stored so
as to apply only to terms with the nonrecursive function symbol OR.


WARNING:  Note that the rewrite rule N-O-I-LEMMA4 will be stored so
as to apply only to terms with the nonrecursive function symbol OR.


WARNING:  Note that the rewrite rule INVERSE-OF-INVERSE will be
stored so as to apply only to terms with the nonrecursive function
symbol INVERSE.


WARNING:  Note that the rewrite rule N-Z-I-LEMMA will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.


WARNING:  Note that the rewrite rule NON-ZEROP-INVERSE will be stored
so as to apply only to terms with the nonrecursive function symbol
ZEROP.


WARNING:  Note that the linear lemma BOUNDED-INVERSE is being stored
under the term (INVERSE J P), which is unusual because INVERSE is a
nonrecursive function symbol.


WARNING:  Note that the rewrite rule INVERSE-1 will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.


WARNING:  the newly proposed lemma, ALL-DISTINCT-INVERSE-LIST, could
be applied whenever the previously added lemma A-D-I-L-LEMMA3 could.




WARNING:  Note that NONZEROP-LESSEQP-ZERO contains the free variable
N which will be chosen by instantiating the hypothesis (ZEROP N).